(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x2F34991EFA1E2318) #xD0CB66E105E1DCE7))
(constraint (= (f #x007D556A3F0E2C1C) #xFF82AA95C0F1D3E3))
(constraint (= (f #x27FA9DF2D2B0C0AA) #xD805620D2D4F3F55))
(constraint (= (f #xEBE6702FB7FCB068) #x14198FD048034F97))
(constraint (= (f #x8256C84538746248) #x7DA937BAC78B9DB7))
(constraint (= (f #x000000000000002A) #xFFFFFFFFFFFFFFD5))
(constraint (= (f #x0000000000000024) #xFFFFFFFFFFFFFFDB))
(constraint (= (f #x000000000000002E) #xFFFFFFFFFFFFFFD1))
(constraint (= (f #x0000000000000034) #xFFFFFFFFFFFFFFCB))
(constraint (= (f #x0000000000000032) #xFFFFFFFFFFFFFFCD))
(constraint (= (f #x9AC4235BDB8C2255) #x00009AC4235BDB8C))
(constraint (= (f #x1ACE9F8EE5B68635) #x00001ACE9F8EE5B6))
(constraint (= (f #x8123FFA4DA734F8A) #x00008123FFA4DA73))
(constraint (= (f #x9682C888ED91A8B7) #x00009682C888ED91))
(constraint (= (f #x9A60731D2E5D23C7) #x00009A60731D2E5D))
(constraint (= (f #xCCCCCCCCCCCCCCCE) #x3333333333333331))
(constraint (= (f #x0000000000000021) #x0000000000000000))
(constraint (= (f #x0000000000000027) #x0000000000000000))
(constraint (= (f #x000000000000003F) #x0000000000000000))
(constraint (= (f #x0000000000000025) #x0000000000000000))
(constraint (= (f #x000000000000003B) #x0000000000000000))
(constraint (= (f #x0000000000000001) #x0000000000000000))
(constraint (= (f #xFFFFFFFFFFFFFFFD) #x0000FFFFFFFFFFFF))
(constraint (= (f #x9BB79716AE626E96) #x644868E9519D9169))
(constraint (= (f #xF1C242483713DC9B) #x0000F1C242483713))
(constraint (= (f #xD4E49F9B3519297B) #x0000D4E49F9B3519))
(constraint (= (f #x7CF22541C1E29840) #x830DDABE3E1D67BF))
(constraint (= (f #x12D4E54FDD614B21) #x000012D4E54FDD61))
(constraint (= (f #x5A146FA521E91C24) #x00005A146FA521E9))
(constraint (= (f #xDF098CFDB394E366) #x20F673024C6B1C99))
(constraint (= (f #x51AFE024295249B5) #x000051AFE0242952))
(constraint (= (f #xB71507C4560CB9A7) #x0000B71507C4560C))
(constraint (= (f #x0A51DD99CE22A720) #xF5AE226631DD58DF))
(constraint (= (f #x0000000000000001) #x0000000000000000))
(constraint (= (f #x0000000000000034) #xFFFFFFFFFFFFFFCB))
(constraint (= (f #xFFFFFFFFFFFFFFFD) #x0000FFFFFFFFFFFF))
(constraint (= (f #xCCCCCCCCCCCCCCCE) #x3333333333333331))
(constraint (= (f #x000000000000002F) #x0000000000000000))
(constraint (= (f #x1F1B3A542601310E) #x00001F1B3A542601))
(constraint (= (f #x5D98707EE658CAD1) #x00005D98707EE658))
(constraint (= (f #xBED4C149F7503A43) #x0000BED4C149F750))
(constraint (= (f #xA83A183BEED6987F) #x0000A83A183BEED6))
(constraint (= (f #x3584B9E65A2CB887) #x00003584B9E65A2C))
(constraint (= (f #x463BA626BFD6CC9D) #x0000463BA626BFD6))
(constraint (= (f #x3AF10C59230EA4AB) #x00003AF10C59230E))
(constraint (= (f #x784CAEF1EB3B50CA) #x0000784CAEF1EB3B))
(constraint (= (f #x832F086E53C3B7A6) #x0000832F086E53C3))
(constraint (= (f #xC4C7F5E1F65BC0DE) #x0000C4C7F5E1F65B))
(check-synth)
